[ENH] Add a tool to reason through the state space of bootstrap. #4558
Conversation
Reviewer ChecklistPlease leverage this checklist to ensure your code review is thorough before approving Testing, Bugs, Errors, Logs, Documentation
System Compatibility
Quality
|
|
Add standalone Rust example to exhaustively reason about WAL bootstrap states Adds Key Changes: Affected Areas: This summary was automatically generated by @propel-code-bot |
![propel-code-bot[bot]](https://avatars.githubusercontent.com/in/1179004?s=60&v=4){kind=small}
| #[derive(Clone, Copy, Debug)] | ||
| enum FragmentState { | ||
| BenignRace, | ||
| Conflict, | ||
| Success, | ||
| } |
There was a problem hiding this comment.
[BestPractice]
Consider adding #[derive(PartialEq, Eq)] to all enum types since they're being compared with matches!. This improves code readability and future-proofs the enums if you need to use equality checks elsewhere.
| } | ||
| } | ||
|
|
||
| enum Disposition { |
There was a problem hiding this comment.
[BestPractice]
The Disposition enum would benefit from adding #[derive(Debug)] to improve debugging if needed. Since it contains other Debug-derived types, this would be straightforward.
There was a problem hiding this comment.
Pull Request Overview
Adds a new example tool that exhaustively explores all combinations of fragment, initialization, and recovery states during bootstrap, classifying each as good, dropped, panicked, or raised.
- Introduces three enums (
FragmentState,InitializeManifest,RecoverManifest) and aDispositionenum - Implements rules (
happy_paths,conflict_on_fragment,error_paths,unconditionally_raise) to categorize each state triple - Adds a
mainthat iterates through all states and applies rules, printing panics and raises
Comments suppressed due to low confidence (1)
rust/wal3/examples/wal3-bootstrap-reasoner.rs:102
- [nitpick] Function
error_pathsemits panic dispositions; consider renaming it topanic_pathsor similar to more accurately reflect its behavior.
fn error_paths(fs: FragmentState, im: InitializeManifest, rm: RecoverManifest) -> Disposition {
| println!("panic({fs:?}, {im:?}, {rm:?}) -> {reason}"); | ||
| break; | ||
| } | ||
| Disposition::Drop(_, _, _, _) => { | ||
| break; | ||
| } | ||
| Disposition::Raise(reason, fs, im, rm) => { | ||
| println!("raise({fs:?}, {im:?}, {rm:?}) -> {reason}"); |
There was a problem hiding this comment.
Invalid use of named formatting placeholders without supplying the corresponding arguments. Consider using positional placeholders with arguments, e.g. println!("panic({:?}, {:?}, {:?}) -> {}", fs, im, rm, reason);.
| println!("panic({fs:?}, {im:?}, {rm:?}) -> {reason}"); | |
| break; | |
| } | |
| Disposition::Drop(_, _, _, _) => { | |
| break; | |
| } | |
| Disposition::Raise(reason, fs, im, rm) => { | |
| println!("raise({fs:?}, {im:?}, {rm:?}) -> {reason}"); | |
| println!("panic({:?}, {:?}, {:?}) -> {}", fs, im, rm, reason); | |
| break; | |
| } | |
| Disposition::Drop(_, _, _, _) => { | |
| break; | |
| } | |
| Disposition::Raise(reason, fs, im, rm) => { | |
| println!("raise({:?}, {:?}, {:?}) -> {}", fs, im, rm, reason); |
Copilot uses AI. Check for mistakes.
| break; | ||
| } | ||
| Disposition::Raise(reason, fs, im, rm) => { | ||
| println!("raise({fs:?}, {im:?}, {rm:?}) -> {reason}"); |
There was a problem hiding this comment.
Invalid use of named formatting placeholders without supplying the corresponding arguments. Consider using positional placeholders with arguments, e.g. println!("raise({:?}, {:?}, {:?}) -> {}", fs, im, rm, reason);.
| println!("raise({fs:?}, {im:?}, {rm:?}) -> {reason}"); | |
| println!("raise({:?}, {:?}, {:?}) -> {}", fs, im, rm, reason); |
Copilot uses AI. Check for mistakes.
The space of cases I have to handle: panic(BenignRace, AlreadyInitialized, Uninitialized) -> cannot double-initialize manifest panic(BenignRace, AlreadyInitialized, Failure) -> cannot double-initialize manifest panic(BenignRace, AlreadyInitialized, Success) -> cannot double-initialize manifest panic(Success, AlreadyInitialized, Uninitialized) -> cannot double-initialize manifest panic(Success, AlreadyInitialized, Failure) -> cannot double-initialize manifest panic(Success, AlreadyInitialized, Success) -> cannot double-initialize manifest panic(BenignRace, Uninitialized, Failure) -> failed to install recovered manifest panic(BenignRace, Success, Failure) -> failed to install recovered manifest panic(Success, Uninitialized, Failure) -> failed to install recovered manifest panic(Success, Success, Failure) -> failed to install recovered manifest panic(BenignRace, Uninitialized, Uninitialized) -> cannot have manifest become uninitialized panic(BenignRace, Success, Uninitialized) -> cannot have manifest become uninitialized panic(Success, Uninitialized, Uninitialized) -> cannot have manifest become uninitialized panic(Success, Success, Uninitialized) -> cannot have manifest become uninitialized Committing so I don't lose it.
rescrv
force-pushed
the
rescrv/wal3-bootstrap
branch
from
cd14dcb to
307051a
Compare
## Description of changes This adds a "bootstrap" call to wal3 that copies the data semi-atomically. It is reasoned to be safe to do concurrent with all other log operations, but may leave a FragmentSeqNo(1) lying around in the event that a log is initialized at the same time it's bootstrapping. This should never happen in our system so thankfully we can just leave the hole. See #4558 for the reasoning. ## Test plan - [ ] Tests pass locally with `pytest` for python, `yarn test` for js, `cargo test` for rust ## Documentation Changes N/A
Description of changes
The space of cases I have to handle:
panic(BenignRace, AlreadyInitialized, Uninitialized) -> cannot double-initialize manifest
panic(BenignRace, AlreadyInitialized, Failure) -> cannot double-initialize manifest
panic(BenignRace, AlreadyInitialized, Success) -> cannot double-initialize manifest
panic(Success, AlreadyInitialized, Uninitialized) -> cannot double-initialize manifest
panic(Success, AlreadyInitialized, Failure) -> cannot double-initialize manifest
panic(Success, AlreadyInitialized, Success) -> cannot double-initialize manifest
panic(BenignRace, Uninitialized, Failure) -> failed to install recovered manifest
panic(BenignRace, Success, Failure) -> failed to install recovered manifest
panic(Success, Uninitialized, Failure) -> failed to install recovered manifest
panic(Success, Success, Failure) -> failed to install recovered manifest
panic(BenignRace, Uninitialized, Uninitialized) -> cannot have manifest become uninitialized
panic(BenignRace, Success, Uninitialized) -> cannot have manifest become uninitialized
panic(Success, Uninitialized, Uninitialized) -> cannot have manifest become uninitialized
panic(Success, Success, Uninitialized) -> cannot have manifest become uninitialized
Committing so I don't lose it.
Test plan
This is a planning tool. It doesn't need testing as it's part of a testing effort.
Documentation Changes
No docs here.